The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(0(2(x1)))) → 0(0(3(1(2(x1)))))
0(1(3(4(x1)))) → 0(4(1(0(3(x1)))))
0(1(3(4(x1)))) → 0(4(1(1(3(x1)))))
0(1(3(4(x1)))) → 0(4(1(3(1(x1)))))
0(2(1(4(x1)))) → 0(4(1(2(3(x1)))))
0(2(1(4(x1)))) → 0(4(1(3(2(x1)))))
0(2(1(4(x1)))) → 2(0(4(1(4(x1)))))
0(2(1(4(x1)))) → 5(5(0(4(1(2(x1))))))
0(2(1(5(x1)))) → 5(0(4(1(2(x1)))))
0(2(2(4(x1)))) → 0(4(2(2(5(x1)))))
0(2(2(4(x1)))) → 0(4(2(5(2(x1)))))
3(4(0(2(x1)))) → 3(0(4(5(2(x1)))))
3(4(0(2(x1)))) → 3(5(0(4(2(x1)))))
0(0(1(4(5(x1))))) → 0(4(1(0(3(5(x1))))))
0(1(0(2(4(x1))))) → 2(0(0(4(1(1(x1))))))
0(1(2(3(4(x1))))) → 2(0(4(1(0(3(x1))))))
0(1(3(3(4(x1))))) → 0(0(3(1(3(4(x1))))))
0(1(4(0(2(x1))))) → 0(4(1(5(0(2(x1))))))
0(1(4(1(5(x1))))) → 2(5(0(4(1(1(x1))))))
0(1(4(3(4(x1))))) → 0(4(0(3(1(4(x1))))))
0(1(4(3(4(x1))))) → 3(0(4(1(5(4(x1))))))
0(1(4(3(5(x1))))) → 5(4(5(0(3(1(x1))))))
0(1(5(0(2(x1))))) → 0(0(4(1(2(5(x1))))))
0(1(5(1(4(x1))))) → 4(5(0(3(1(1(x1))))))
0(2(1(4(4(x1))))) → 0(4(1(2(4(3(x1))))))
0(2(1(4(5(x1))))) → 0(4(1(2(5(2(x1))))))
0(2(1(5(4(x1))))) → 5(0(2(0(4(1(x1))))))
0(2(4(1(5(x1))))) → 5(0(4(1(5(2(x1))))))
0(2(4(3(5(x1))))) → 0(4(5(2(5(3(x1))))))
0(2(5(1(4(x1))))) → 0(0(5(4(1(2(x1))))))
3(0(1(3(2(x1))))) → 0(3(1(0(3(2(x1))))))
3(0(2(1(4(x1))))) → 4(0(4(1(3(2(x1))))))
3(0(2(1(5(x1))))) → 5(3(2(0(4(1(x1))))))
3(0(4(0(2(x1))))) → 0(3(4(0(4(2(x1))))))
3(0(4(0(2(x1))))) → 0(4(1(2(0(3(x1))))))
3(0(5(1(4(x1))))) → 3(0(4(1(1(5(x1))))))
3(0(5(1(5(x1))))) → 0(4(1(3(5(5(x1))))))
3(2(4(1(2(x1))))) → 3(1(2(2(5(4(x1))))))
3(2(4(1(5(x1))))) → 3(1(4(5(2(5(x1))))))
3(4(0(1(2(x1))))) → 0(4(2(0(3(1(x1))))))
3(4(0(1(4(x1))))) → 0(4(1(5(3(4(x1))))))
3(4(0(1(5(x1))))) → 0(4(1(5(5(3(x1))))))
3(4(0(2(4(x1))))) → 0(3(4(0(4(2(x1))))))
3(4(1(2(4(x1))))) → 0(4(1(2(4(3(x1))))))
3(4(1(3(5(x1))))) → 4(3(0(3(1(5(x1))))))
3(4(3(0(2(x1))))) → 3(3(0(4(1(2(x1))))))
3(4(5(0(2(x1))))) → 0(3(0(4(2(5(x1))))))
3(5(0(2(2(x1))))) → 0(3(2(5(2(5(x1))))))
3(5(2(1(4(x1))))) → 3(5(1(0(4(2(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(1(0(2(z0)))) → c(0'(0(3(1(2(z0))))), 0'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(1(3(4(z0)))) → c3(0'(4(1(3(1(z0))))), 3'(1(z0)))
0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(2(1(4(z0)))) → c5(0'(4(1(3(2(z0))))), 3'(2(z0)))
0'(2(1(4(z0)))) → c6(0'(4(1(4(z0)))))
0'(2(1(4(z0)))) → c7(0'(4(1(2(z0)))))
0'(2(1(5(z0)))) → c8(0'(4(1(2(z0)))))
0'(2(2(4(z0)))) → c9(0'(4(2(2(5(z0))))))
0'(2(2(4(z0)))) → c10(0'(4(2(5(2(z0))))))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(0(2(4(z0))))) → c12(0'(0(4(1(1(z0))))), 0'(4(1(1(z0)))))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(1(4(1(5(z0))))) → c16(0'(4(1(1(z0)))))
0'(1(4(3(4(z0))))) → c17(0'(4(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))))
0'(1(4(3(4(z0))))) → c18(3'(0(4(1(5(4(z0)))))), 0'(4(1(5(4(z0))))))
0'(1(4(3(5(z0))))) → c19(0'(3(1(z0))), 3'(1(z0)))
0'(1(5(0(2(z0))))) → c20(0'(0(4(1(2(5(z0)))))), 0'(4(1(2(5(z0))))))
0'(1(5(1(4(z0))))) → c21(0'(3(1(1(z0)))), 3'(1(1(z0))))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
0'(2(1(4(5(z0))))) → c23(0'(4(1(2(5(2(z0)))))))
0'(2(1(5(4(z0))))) → c24(0'(2(0(4(1(z0))))), 0'(4(1(z0))))
0'(2(4(1(5(z0))))) → c25(0'(4(1(5(2(z0))))))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))
0'(2(5(1(4(z0))))) → c27(0'(0(5(4(1(2(z0)))))), 0'(5(4(1(2(z0))))))
3'(4(0(2(z0)))) → c28(3'(0(4(5(2(z0))))), 0'(4(5(2(z0)))))
3'(4(0(2(z0)))) → c29(3'(5(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(1(3(2(z0))))) → c30(0'(3(1(0(3(2(z0)))))), 3'(1(0(3(2(z0))))), 0'(3(2(z0))), 3'(2(z0)))
3'(0(2(1(4(z0))))) → c31(0'(4(1(3(2(z0))))), 3'(2(z0)))
3'(0(2(1(5(z0))))) → c32(3'(2(0(4(1(z0))))), 0'(4(1(z0))))
3'(0(4(0(2(z0))))) → c33(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(0(5(1(4(z0))))) → c35(3'(0(4(1(1(5(z0)))))), 0'(4(1(1(5(z0))))))
3'(0(5(1(5(z0))))) → c36(0'(4(1(3(5(5(z0)))))), 3'(5(5(z0))))
3'(2(4(1(2(z0))))) → c37(3'(1(2(2(5(4(z0)))))))
3'(2(4(1(5(z0))))) → c38(3'(1(4(5(2(5(z0)))))))
3'(4(0(1(2(z0))))) → c39(0'(4(2(0(3(1(z0)))))), 0'(3(1(z0))), 3'(1(z0)))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
3'(4(0(2(4(z0))))) → c42(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(4(1(3(5(z0))))) → c44(3'(0(3(1(5(z0))))), 0'(3(1(5(z0)))), 3'(1(5(z0))))
3'(4(3(0(2(z0))))) → c45(3'(3(0(4(1(2(z0)))))), 3'(0(4(1(2(z0))))), 0'(4(1(2(z0)))))
3'(4(5(0(2(z0))))) → c46(0'(3(0(4(2(5(z0)))))), 3'(0(4(2(5(z0))))), 0'(4(2(5(z0)))))
3'(5(0(2(2(z0))))) → c47(0'(3(2(5(2(5(z0)))))), 3'(2(5(2(5(z0))))))
3'(5(2(1(4(z0))))) → c48(3'(5(1(0(4(2(z0)))))), 0'(4(2(z0))))

S tuples:

0'(1(0(2(z0)))) → c(0'(0(3(1(2(z0))))), 0'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(1(3(4(z0)))) → c3(0'(4(1(3(1(z0))))), 3'(1(z0)))
0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(2(1(4(z0)))) → c5(0'(4(1(3(2(z0))))), 3'(2(z0)))
0'(2(1(4(z0)))) → c6(0'(4(1(4(z0)))))
0'(2(1(4(z0)))) → c7(0'(4(1(2(z0)))))
0'(2(1(5(z0)))) → c8(0'(4(1(2(z0)))))
0'(2(2(4(z0)))) → c9(0'(4(2(2(5(z0))))))
0'(2(2(4(z0)))) → c10(0'(4(2(5(2(z0))))))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(0(2(4(z0))))) → c12(0'(0(4(1(1(z0))))), 0'(4(1(1(z0)))))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(1(4(1(5(z0))))) → c16(0'(4(1(1(z0)))))
0'(1(4(3(4(z0))))) → c17(0'(4(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))))
0'(1(4(3(4(z0))))) → c18(3'(0(4(1(5(4(z0)))))), 0'(4(1(5(4(z0))))))
0'(1(4(3(5(z0))))) → c19(0'(3(1(z0))), 3'(1(z0)))
0'(1(5(0(2(z0))))) → c20(0'(0(4(1(2(5(z0)))))), 0'(4(1(2(5(z0))))))
0'(1(5(1(4(z0))))) → c21(0'(3(1(1(z0)))), 3'(1(1(z0))))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
0'(2(1(4(5(z0))))) → c23(0'(4(1(2(5(2(z0)))))))
0'(2(1(5(4(z0))))) → c24(0'(2(0(4(1(z0))))), 0'(4(1(z0))))
0'(2(4(1(5(z0))))) → c25(0'(4(1(5(2(z0))))))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))
0'(2(5(1(4(z0))))) → c27(0'(0(5(4(1(2(z0)))))), 0'(5(4(1(2(z0))))))
3'(4(0(2(z0)))) → c28(3'(0(4(5(2(z0))))), 0'(4(5(2(z0)))))
3'(4(0(2(z0)))) → c29(3'(5(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(1(3(2(z0))))) → c30(0'(3(1(0(3(2(z0)))))), 3'(1(0(3(2(z0))))), 0'(3(2(z0))), 3'(2(z0)))
3'(0(2(1(4(z0))))) → c31(0'(4(1(3(2(z0))))), 3'(2(z0)))
3'(0(2(1(5(z0))))) → c32(3'(2(0(4(1(z0))))), 0'(4(1(z0))))
3'(0(4(0(2(z0))))) → c33(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(0(5(1(4(z0))))) → c35(3'(0(4(1(1(5(z0)))))), 0'(4(1(1(5(z0))))))
3'(0(5(1(5(z0))))) → c36(0'(4(1(3(5(5(z0)))))), 3'(5(5(z0))))
3'(2(4(1(2(z0))))) → c37(3'(1(2(2(5(4(z0)))))))
3'(2(4(1(5(z0))))) → c38(3'(1(4(5(2(5(z0)))))))
3'(4(0(1(2(z0))))) → c39(0'(4(2(0(3(1(z0)))))), 0'(3(1(z0))), 3'(1(z0)))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
3'(4(0(2(4(z0))))) → c42(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(4(1(3(5(z0))))) → c44(3'(0(3(1(5(z0))))), 0'(3(1(5(z0)))), 3'(1(5(z0))))
3'(4(3(0(2(z0))))) → c45(3'(3(0(4(1(2(z0)))))), 3'(0(4(1(2(z0))))), 0'(4(1(2(z0)))))
3'(4(5(0(2(z0))))) → c46(0'(3(0(4(2(5(z0)))))), 3'(0(4(2(5(z0))))), 0'(4(2(5(z0)))))
3'(5(0(2(2(z0))))) → c47(0'(3(2(5(2(5(z0)))))), 3'(2(5(2(5(z0))))))
3'(5(2(1(4(z0))))) → c48(3'(5(1(0(4(2(z0)))))), 0'(4(2(z0))))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

3'(0(2(1(4(z0))))) → c31(0'(4(1(3(2(z0))))), 3'(2(z0)))
3'(0(2(1(5(z0))))) → c32(3'(2(0(4(1(z0))))), 0'(4(1(z0))))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(2(1(4(z0)))) → c5(0'(4(1(3(2(z0))))), 3'(2(z0)))
0'(2(1(4(z0)))) → c6(0'(4(1(4(z0)))))
0'(2(1(4(z0)))) → c7(0'(4(1(2(z0)))))
0'(2(1(5(z0)))) → c8(0'(4(1(2(z0)))))
0'(2(2(4(z0)))) → c9(0'(4(2(2(5(z0))))))
0'(2(2(4(z0)))) → c10(0'(4(2(5(2(z0))))))
0'(1(4(1(5(z0))))) → c16(0'(4(1(1(z0)))))
0'(1(5(1(4(z0))))) → c21(0'(3(1(1(z0)))), 3'(1(1(z0))))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
0'(2(1(4(5(z0))))) → c23(0'(4(1(2(5(2(z0)))))))
0'(2(1(5(4(z0))))) → c24(0'(2(0(4(1(z0))))), 0'(4(1(z0))))
0'(2(4(1(5(z0))))) → c25(0'(4(1(5(2(z0))))))
0'(2(5(1(4(z0))))) → c27(0'(0(5(4(1(2(z0)))))), 0'(5(4(1(2(z0))))))
3'(2(4(1(2(z0))))) → c37(3'(1(2(2(5(4(z0)))))))
3'(2(4(1(5(z0))))) → c38(3'(1(4(5(2(5(z0)))))))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(5(2(1(4(z0))))) → c48(3'(5(1(0(4(2(z0)))))), 0'(4(2(z0))))
3'(4(0(2(z0)))) → c28(3'(0(4(5(2(z0))))), 0'(4(5(2(z0)))))
3'(4(0(2(z0)))) → c29(3'(5(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(1(3(2(z0))))) → c30(0'(3(1(0(3(2(z0)))))), 3'(1(0(3(2(z0))))), 0'(3(2(z0))), 3'(2(z0)))
3'(0(4(0(2(z0))))) → c33(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(0(5(1(4(z0))))) → c35(3'(0(4(1(1(5(z0)))))), 0'(4(1(1(5(z0))))))
3'(0(5(1(5(z0))))) → c36(0'(4(1(3(5(5(z0)))))), 3'(5(5(z0))))
3'(4(0(1(2(z0))))) → c39(0'(4(2(0(3(1(z0)))))), 0'(3(1(z0))), 3'(1(z0)))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
3'(4(0(2(4(z0))))) → c42(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(4(1(3(5(z0))))) → c44(3'(0(3(1(5(z0))))), 0'(3(1(5(z0)))), 3'(1(5(z0))))
3'(4(3(0(2(z0))))) → c45(3'(3(0(4(1(2(z0)))))), 3'(0(4(1(2(z0))))), 0'(4(1(2(z0)))))
3'(4(5(0(2(z0))))) → c46(0'(3(0(4(2(5(z0)))))), 3'(0(4(2(5(z0))))), 0'(4(2(5(z0)))))
3'(5(0(2(2(z0))))) → c47(0'(3(2(5(2(5(z0)))))), 3'(2(5(2(5(z0))))))
0'(1(0(2(z0)))) → c(0'(0(3(1(2(z0))))), 0'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(1(3(4(z0)))) → c3(0'(4(1(3(1(z0))))), 3'(1(z0)))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(0(2(4(z0))))) → c12(0'(0(4(1(1(z0))))), 0'(4(1(1(z0)))))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(1(4(3(4(z0))))) → c17(0'(4(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))))
0'(1(4(3(4(z0))))) → c18(3'(0(4(1(5(4(z0)))))), 0'(4(1(5(4(z0))))))
0'(1(4(3(5(z0))))) → c19(0'(3(1(z0))), 3'(1(z0)))
0'(1(5(0(2(z0))))) → c20(0'(0(4(1(2(5(z0)))))), 0'(4(1(2(5(z0))))))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))

S tuples:

0'(1(0(2(z0)))) → c(0'(0(3(1(2(z0))))), 0'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(1(3(4(z0)))) → c3(0'(4(1(3(1(z0))))), 3'(1(z0)))
0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(2(1(4(z0)))) → c5(0'(4(1(3(2(z0))))), 3'(2(z0)))
0'(2(1(4(z0)))) → c6(0'(4(1(4(z0)))))
0'(2(1(4(z0)))) → c7(0'(4(1(2(z0)))))
0'(2(1(5(z0)))) → c8(0'(4(1(2(z0)))))
0'(2(2(4(z0)))) → c9(0'(4(2(2(5(z0))))))
0'(2(2(4(z0)))) → c10(0'(4(2(5(2(z0))))))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(0(2(4(z0))))) → c12(0'(0(4(1(1(z0))))), 0'(4(1(1(z0)))))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(1(4(1(5(z0))))) → c16(0'(4(1(1(z0)))))
0'(1(4(3(4(z0))))) → c17(0'(4(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))))
0'(1(4(3(4(z0))))) → c18(3'(0(4(1(5(4(z0)))))), 0'(4(1(5(4(z0))))))
0'(1(4(3(5(z0))))) → c19(0'(3(1(z0))), 3'(1(z0)))
0'(1(5(0(2(z0))))) → c20(0'(0(4(1(2(5(z0)))))), 0'(4(1(2(5(z0))))))
0'(1(5(1(4(z0))))) → c21(0'(3(1(1(z0)))), 3'(1(1(z0))))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
0'(2(1(4(5(z0))))) → c23(0'(4(1(2(5(2(z0)))))))
0'(2(1(5(4(z0))))) → c24(0'(2(0(4(1(z0))))), 0'(4(1(z0))))
0'(2(4(1(5(z0))))) → c25(0'(4(1(5(2(z0))))))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))
0'(2(5(1(4(z0))))) → c27(0'(0(5(4(1(2(z0)))))), 0'(5(4(1(2(z0))))))
3'(4(0(2(z0)))) → c28(3'(0(4(5(2(z0))))), 0'(4(5(2(z0)))))
3'(4(0(2(z0)))) → c29(3'(5(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(1(3(2(z0))))) → c30(0'(3(1(0(3(2(z0)))))), 3'(1(0(3(2(z0))))), 0'(3(2(z0))), 3'(2(z0)))
3'(0(4(0(2(z0))))) → c33(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(0(5(1(4(z0))))) → c35(3'(0(4(1(1(5(z0)))))), 0'(4(1(1(5(z0))))))
3'(0(5(1(5(z0))))) → c36(0'(4(1(3(5(5(z0)))))), 3'(5(5(z0))))
3'(2(4(1(2(z0))))) → c37(3'(1(2(2(5(4(z0)))))))
3'(2(4(1(5(z0))))) → c38(3'(1(4(5(2(5(z0)))))))
3'(4(0(1(2(z0))))) → c39(0'(4(2(0(3(1(z0)))))), 0'(3(1(z0))), 3'(1(z0)))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
3'(4(0(2(4(z0))))) → c42(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(4(1(3(5(z0))))) → c44(3'(0(3(1(5(z0))))), 0'(3(1(5(z0)))), 3'(1(5(z0))))
3'(4(3(0(2(z0))))) → c45(3'(3(0(4(1(2(z0)))))), 3'(0(4(1(2(z0))))), 0'(4(1(2(z0)))))
3'(4(5(0(2(z0))))) → c46(0'(3(0(4(2(5(z0)))))), 3'(0(4(2(5(z0))))), 0'(4(2(5(z0)))))
3'(5(0(2(2(z0))))) → c47(0'(3(2(5(2(5(z0)))))), 3'(2(5(2(5(z0))))))
3'(5(2(1(4(z0))))) → c48(3'(5(1(0(4(2(z0)))))), 0'(4(2(z0))))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c5, c6, c7, c8, c9, c10, c16, c21, c22, c23, c24, c25, c27, c37, c38, c43, c48, c28, c29, c30, c33, c34, c35, c36, c39, c40, c41, c42, c44, c45, c46, c47, c, c1, c2, c3, c11, c12, c13, c14, c15, c17, c18, c19, c20, c26

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 34 of 47 dangling nodes:

0'(1(0(2(z0)))) → c(0'(0(3(1(2(z0))))), 0'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(3(4(z0)))) → c3(0'(4(1(3(1(z0))))), 3'(1(z0)))
0'(2(1(4(z0)))) → c5(0'(4(1(3(2(z0))))), 3'(2(z0)))
0'(2(1(4(z0)))) → c6(0'(4(1(4(z0)))))
0'(2(1(4(z0)))) → c7(0'(4(1(2(z0)))))
0'(2(1(5(z0)))) → c8(0'(4(1(2(z0)))))
0'(2(2(4(z0)))) → c9(0'(4(2(2(5(z0))))))
0'(2(2(4(z0)))) → c10(0'(4(2(5(2(z0))))))
0'(1(0(2(4(z0))))) → c12(0'(0(4(1(1(z0))))), 0'(4(1(1(z0)))))
0'(1(4(1(5(z0))))) → c16(0'(4(1(1(z0)))))
0'(1(4(3(4(z0))))) → c18(3'(0(4(1(5(4(z0)))))), 0'(4(1(5(4(z0))))))
0'(1(4(3(4(z0))))) → c17(0'(4(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))))
0'(1(5(0(2(z0))))) → c20(0'(0(4(1(2(5(z0)))))), 0'(4(1(2(5(z0))))))
0'(1(4(3(5(z0))))) → c19(0'(3(1(z0))), 3'(1(z0)))
0'(1(5(1(4(z0))))) → c21(0'(3(1(1(z0)))), 3'(1(1(z0))))
0'(2(1(5(4(z0))))) → c24(0'(2(0(4(1(z0))))), 0'(4(1(z0))))
0'(2(1(4(5(z0))))) → c23(0'(4(1(2(5(2(z0)))))))
0'(2(4(1(5(z0))))) → c25(0'(4(1(5(2(z0))))))
3'(4(0(2(z0)))) → c28(3'(0(4(5(2(z0))))), 0'(4(5(2(z0)))))
0'(2(5(1(4(z0))))) → c27(0'(0(5(4(1(2(z0)))))), 0'(5(4(1(2(z0))))))
3'(0(1(3(2(z0))))) → c30(0'(3(1(0(3(2(z0)))))), 3'(1(0(3(2(z0))))), 0'(3(2(z0))), 3'(2(z0)))
3'(4(0(2(z0)))) → c29(3'(5(0(4(2(z0))))), 0'(4(2(z0))))
3'(0(4(0(2(z0))))) → c33(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(2(4(1(2(z0))))) → c37(3'(1(2(2(5(4(z0)))))))
3'(2(4(1(5(z0))))) → c38(3'(1(4(5(2(5(z0)))))))
3'(0(5(1(4(z0))))) → c35(3'(0(4(1(1(5(z0)))))), 0'(4(1(1(5(z0))))))
3'(0(5(1(5(z0))))) → c36(0'(4(1(3(5(5(z0)))))), 3'(5(5(z0))))
3'(4(0(2(4(z0))))) → c42(0'(3(4(0(4(2(z0)))))), 3'(4(0(4(2(z0))))), 0'(4(2(z0))))
3'(4(0(1(2(z0))))) → c39(0'(4(2(0(3(1(z0)))))), 0'(3(1(z0))), 3'(1(z0)))
3'(4(3(0(2(z0))))) → c45(3'(3(0(4(1(2(z0)))))), 3'(0(4(1(2(z0))))), 0'(4(1(2(z0)))))
3'(4(5(0(2(z0))))) → c46(0'(3(0(4(2(5(z0)))))), 3'(0(4(2(5(z0))))), 0'(4(2(5(z0)))))
3'(4(1(3(5(z0))))) → c44(3'(0(3(1(5(z0))))), 0'(3(1(5(z0)))), 3'(1(5(z0))))
3'(5(2(1(4(z0))))) → c48(3'(5(1(0(4(2(z0)))))), 0'(4(2(z0))))
3'(5(0(2(2(z0))))) → c47(0'(3(2(5(2(5(z0)))))), 3'(2(5(2(5(z0))))))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))

S tuples:

0'(1(3(4(z0)))) → c1(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(0'(4(1(1(3(z0))))), 3'(z0))
0'(2(1(4(z0)))) → c4(0'(4(1(2(3(z0))))), 3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(4(1(0(3(5(z0)))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(2(3(4(z0))))) → c13(0'(4(1(0(3(z0))))), 0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(0'(0(3(1(3(4(z0)))))), 0'(3(1(3(4(z0))))), 3'(1(3(4(z0)))), 3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(4(1(5(0(2(z0)))))), 0'(2(z0)))
0'(2(1(4(4(z0))))) → c22(0'(4(1(2(4(3(z0)))))), 3'(z0))
0'(2(4(3(5(z0))))) → c26(0'(4(5(2(5(3(z0)))))), 3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(4(1(2(0(3(z0)))))), 0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(0'(4(1(5(3(4(z0)))))), 3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(0'(4(1(5(5(3(z0)))))), 3'(z0))
3'(4(1(2(4(z0))))) → c43(0'(4(1(2(4(3(z0)))))), 3'(z0))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 16 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = [4]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(3(4(z0)))) → c2(3'(z0))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [4]x₁   
POL(1(x₁)) = [1]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(3(3(4(z0))))) → c14(3'(4(z0)))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = [1]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = [4]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(4(0(2(z0))))) → c15(0'(2(z0)))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [4]x₁   
POL(1(x₁)) = [1]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(2(4(3(5(z0))))) → c26(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
0'(2(4(3(5(z0))))) → c26(3'(z0))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [4]x₁   
POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = [4]   
POL(2(x₁)) = [4]   
POL(3(x₁)) = 0   
POL(3'(x₁)) = [4]   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
0'(2(4(3(5(z0))))) → c26(3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))

We considered the (Usable) Rules:

3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))

And the Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2]x₁   
POL(0'(x₁)) = [4]x₁   
POL(1(x₁)) = [2]   
POL(2(x₁)) = 0   
POL(3(x₁)) = 0   
POL(3'(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = [4]   
POL(c1(x₁, x₂)) = x₁ + x₂   
POL(c11(x₁)) = x₁   
POL(c13(x₁, x₂)) = x₁ + x₂   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c34(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
0'(2(4(3(5(z0))))) → c26(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c34, c40, c41, c1, c2, c11, c13, c14, c15, c26

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 3'(0(4(0(2(z0))))) → c34(0'(3(z0)), 3'(z0)) by

3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))

K tuples:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
0'(2(4(3(5(z0))))) → c26(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c40, c41, c1, c2, c11, c13, c14, c15, c26, c34

(25) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

0'(1(3(4(z0)))) → c1(0'(3(z0)), 3'(z0))
0'(1(3(4(z0)))) → c2(3'(z0))
0'(0(1(4(5(z0))))) → c11(0'(3(5(z0))))
0'(1(2(3(4(z0))))) → c13(0'(3(z0)), 3'(z0))
0'(1(3(3(4(z0))))) → c14(3'(4(z0)))
0'(1(4(0(2(z0))))) → c15(0'(2(z0)))
0'(2(4(3(5(z0))))) → c26(3'(z0))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))
3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))

K tuples:

0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

0', 3'

Compound Symbols:

c4, c22, c43, c40, c41, c34

(27) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 14 of 22 dangling nodes:

3'(0(4(0(2(4(5(0(2(z0))))))))) → c34(0'(0(3(0(4(2(5(z0))))))), 3'(4(5(0(2(z0))))))
3'(0(4(0(2(5(0(2(2(z0))))))))) → c34(0'(0(3(2(5(2(5(z0))))))), 3'(5(0(2(2(z0))))))
3'(0(4(0(2(4(1(3(5(z0))))))))) → c34(0'(4(3(0(3(1(5(z0))))))), 3'(4(1(3(5(z0))))))
3'(0(4(0(2(4(3(0(2(z0))))))))) → c34(0'(3(3(0(4(1(2(z0))))))), 3'(4(3(0(2(z0))))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(5(0(4(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(4(0(2(z0)))))))) → c34(0'(3(0(4(5(2(z0)))))), 3'(4(0(2(z0)))))
3'(0(4(0(2(5(2(1(4(z0))))))))) → c34(0'(3(5(1(0(4(2(z0))))))), 3'(5(2(1(4(z0))))))
3'(0(4(0(2(0(1(3(2(z0))))))))) → c34(0'(0(3(1(0(3(2(z0))))))), 3'(0(1(3(2(z0))))))
3'(0(4(0(2(0(5(1(5(z0))))))))) → c34(0'(0(4(1(3(5(5(z0))))))), 3'(0(5(1(5(z0))))))
3'(0(4(0(2(4(0(1(2(z0))))))))) → c34(0'(0(4(2(0(3(1(z0))))))), 3'(4(0(1(2(z0))))))
3'(0(4(0(2(0(5(1(4(z0))))))))) → c34(0'(3(0(4(1(1(5(z0))))))), 3'(0(5(1(4(z0))))))
3'(0(4(0(2(4(0(2(4(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(4(0(2(4(z0))))))
0'(2(1(4(z0)))) → c4(3'(z0))
0'(2(1(4(4(z0))))) → c22(3'(z0))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(3(4(0(4(2(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(0'(0(4(1(2(0(3(z0))))))), 3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(0'(0(4(1(5(3(4(z0))))))), 3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(0'(0(4(1(5(5(3(z0))))))), 3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(0'(0(4(1(2(4(3(z0))))))), 3'(4(1(2(4(z0))))))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

3'

Compound Symbols:

c43, c40, c41, c34

(29) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

S tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

K tuples:none
Defined Rule Symbols:

0, 3

Defined Pair Symbols:

3'

Compound Symbols:

c43, c40, c41, c34

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

We considered the (Usable) Rules:none
And the Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [1] + x₁   
POL(3'(x₁)) = [2]x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [1] + x₁   
POL(c34(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

S tuples:

3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))

K tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

3'

Compound Symbols:

c43, c40, c41, c34

(33) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))

We considered the (Usable) Rules:none
And the Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [4] + [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [2] + x₁   
POL(3'(x₁)) = [2]x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [4] + x₁   
POL(c34(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c43(x₁)) = x₁   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(0(2(z0)))) → 0(0(3(1(2(z0)))))
0(1(3(4(z0)))) → 0(4(1(0(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(1(3(z0)))))
0(1(3(4(z0)))) → 0(4(1(3(1(z0)))))
0(2(1(4(z0)))) → 0(4(1(2(3(z0)))))
0(2(1(4(z0)))) → 0(4(1(3(2(z0)))))
0(2(1(4(z0)))) → 2(0(4(1(4(z0)))))
0(2(1(4(z0)))) → 5(5(0(4(1(2(z0))))))
0(2(1(5(z0)))) → 5(0(4(1(2(z0)))))
0(2(2(4(z0)))) → 0(4(2(2(5(z0)))))
0(2(2(4(z0)))) → 0(4(2(5(2(z0)))))
0(0(1(4(5(z0))))) → 0(4(1(0(3(5(z0))))))
0(1(0(2(4(z0))))) → 2(0(0(4(1(1(z0))))))
0(1(2(3(4(z0))))) → 2(0(4(1(0(3(z0))))))
0(1(3(3(4(z0))))) → 0(0(3(1(3(4(z0))))))
0(1(4(0(2(z0))))) → 0(4(1(5(0(2(z0))))))
0(1(4(1(5(z0))))) → 2(5(0(4(1(1(z0))))))
0(1(4(3(4(z0))))) → 0(4(0(3(1(4(z0))))))
0(1(4(3(4(z0))))) → 3(0(4(1(5(4(z0))))))
0(1(4(3(5(z0))))) → 5(4(5(0(3(1(z0))))))
0(1(5(0(2(z0))))) → 0(0(4(1(2(5(z0))))))
0(1(5(1(4(z0))))) → 4(5(0(3(1(1(z0))))))
0(2(1(4(4(z0))))) → 0(4(1(2(4(3(z0))))))
0(2(1(4(5(z0))))) → 0(4(1(2(5(2(z0))))))
0(2(1(5(4(z0))))) → 5(0(2(0(4(1(z0))))))
0(2(4(1(5(z0))))) → 5(0(4(1(5(2(z0))))))
0(2(4(3(5(z0))))) → 0(4(5(2(5(3(z0))))))
0(2(5(1(4(z0))))) → 0(0(5(4(1(2(z0))))))
3(4(0(2(z0)))) → 3(0(4(5(2(z0)))))
3(4(0(2(z0)))) → 3(5(0(4(2(z0)))))
3(0(1(3(2(z0))))) → 0(3(1(0(3(2(z0))))))
3(0(2(1(4(z0))))) → 4(0(4(1(3(2(z0))))))
3(0(2(1(5(z0))))) → 5(3(2(0(4(1(z0))))))
3(0(4(0(2(z0))))) → 0(3(4(0(4(2(z0))))))
3(0(4(0(2(z0))))) → 0(4(1(2(0(3(z0))))))
3(0(5(1(4(z0))))) → 3(0(4(1(1(5(z0))))))
3(0(5(1(5(z0))))) → 0(4(1(3(5(5(z0))))))
3(2(4(1(2(z0))))) → 3(1(2(2(5(4(z0))))))
3(2(4(1(5(z0))))) → 3(1(4(5(2(5(z0))))))
3(4(0(1(2(z0))))) → 0(4(2(0(3(1(z0))))))
3(4(0(1(4(z0))))) → 0(4(1(5(3(4(z0))))))
3(4(0(1(5(z0))))) → 0(4(1(5(5(3(z0))))))
3(4(0(2(4(z0))))) → 0(3(4(0(4(2(z0))))))
3(4(1(2(4(z0))))) → 0(4(1(2(4(3(z0))))))
3(4(1(3(5(z0))))) → 4(3(0(3(1(5(z0))))))
3(4(3(0(2(z0))))) → 3(3(0(4(1(2(z0))))))
3(4(5(0(2(z0))))) → 0(3(0(4(2(5(z0))))))
3(5(0(2(2(z0))))) → 0(3(2(5(2(5(z0))))))
3(5(2(1(4(z0))))) → 3(5(1(0(4(2(z0))))))

Tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))

S tuples:

3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))

K tuples:

3'(4(1(2(4(z0))))) → c43(3'(z0))
3'(0(4(0(2(0(4(0(2(z0))))))))) → c34(3'(0(4(0(2(z0))))))
3'(0(4(0(2(4(0(1(4(z0))))))))) → c34(3'(4(0(1(4(z0))))))
3'(0(4(0(2(4(1(2(4(z0))))))))) → c34(3'(4(1(2(4(z0))))))
3'(4(0(1(4(z0))))) → c40(3'(4(z0)))
3'(4(0(1(5(z0))))) → c41(3'(z0))

Defined Rule Symbols:

0, 3

Defined Pair Symbols:

3'

Compound Symbols:

c43, c40, c41, c34

(35) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

3'(0(4(0(2(4(0(1(5(z0))))))))) → c34(3'(4(0(1(5(z0))))))
3'(4(0(1(5(z0))))) → c41(3'(z0))

Now S is empty

(36) BOUNDS(O(1), O(1))